feat(CondensedMatter): action of crystal symmetries on the Brillouin zone by TomOleDiem · Pull Request #1975 · leanprover-community/physlib

TomOleDiem · 2026-10-27T20:33:37Z

Summary

BrillouinZone G: the dual group of the translations of a crystal, the crystal momenta.
The lattice automorphisms act on it by k ↦ k ∘ A⁻¹.
The symmetries of a crystal act on it through their lattice automorphism.
A symmetry and its point operation act in the same way. Shifts fix every point.

The reduced zone and the irreducible zone are in a follow-up PR.

github-actions · 2026-10-27T20:34:49Z

Thank you for this pull-request (PR). If this is your first PR, welcome to the community!

While you wait for a review, note that you can review PRs too; reviewing is not restricted to maintainers. Our review guidelines explain what to look for.

Over time, contributions such as reviews, maintenance and documentation are recorded on contributions.physlib.io.

Four main points:

Comment -awaiting-author on its own line to remove that label from your PR.
Comment blocked-by-PR or -blocked-by-PR on its own line to add or remove that label, respectively.
The first review might take several days to arrive. If in doubt message on the Zulip.

For the author: Please read

Below is what will happen next. Please read carefully if you are not familiar with the process. You may open other PRs while this one is being reviewed, and can stack PRs on top of each other, so don't let these steps slow you down.

Some automated checks will be run on your PR. You can see the results of these checks at the buttom of your PR page. If any of these checks fail, you will need to fix the issues before your PR can be merged. You can learn more about these here, including how to run them locally, which is sometimes quicker than relying on the GitHub Actions. If you have never had a PR merged before, you may have to wait for a reviewer to manually start these checks (this is for security).
A reviewer will look at your PR and may ask you to make changes. This may happen a couple of days after you submit your PR, so you may need to be patient. But it should not be longer than that - if it is please bring it to the attention of the community on the Zulip. The level of review will depend on where your PR is submitted. If it is submitted to ./Physlib or ./QuantumInfo, the review will be more thorough than if it is submitted to ./PhyslibAlpha. You can find out more about what the review process is looking for in our review guidelines. If a reviewer adds an awaiting-author label to your PR, address the review comments, then please remove that label by adding a comment with -awaiting-author. This helps us keep track of reviews.
The reviewer will either approve your PR, or request more changes (in which case we return to step 2). Once your PR is approved, it will be merged by a maintainer, this should happen shortly after approval, though you may get more comments at this stage.

Tip: The easiest way to get a fast review is to submit a PR that is small and self-contained, and has clear documentation explaining why things are the way they are in your changes.

If you have any problems or questions, please reach out to the community on the Zulip.

For reviewers: Summary of your PR

Found differences:
@@ Physlib.CondensedMatter.Crystal.Symmetry.BrillouinZone @@
+ module added Physlib.CondensedMatter.Crystal.Symmetry.BrillouinZone (+125 -0)
  namespaces Physlib.CondensedMatter.Crystal, Physlib.CondensedMatter.Crystal.BrillouinZone
+ added abbrev BrillouinZone
+ added instance (C : Crystal G) : MulDistribMulAction (Symmetry C) (BrillouinZone G)
+ added instance :
+ added lemma BrillouinZone.smul_apply
+ added lemma pointOp_smul
+ added lemma shift_smul
+ added lemma smul_lattice_apply
@@ Physlib @@
! module modified Physlib (+1 -0)
9 differences

The declarations are found by reading the diff as text, without regard for namespaces, so a declaration whose keyword and name are on different lines is missed, and two declarations of the same name in different namespaces are listed as one. A change to a proof, or to the body of a definition, does not appear. See scripts/alpha/github/pr_summary.lean.

Summary of commit 6bdd292, remade whenever a commit is pushed.

jstoobysmith · 2026-10-29T14:01:33Z

+  PontryaginDual (Multiplicative G)
+
+/-- Precompose `χ` with the lattice automorphism `A`. -/
+noncomputable def dualMap (A : G ≃+ G) (χ : TranslationDual G) : TranslationDual G :=


Symmetry namespace?

jstoobysmith · 2026-10-29T14:03:35Z

+A wave moving through a crystal picks up a phase whenever it is shifted by a lattice vector.
+For a Bloch wave, these phases encode its crystal momentum. Since momenta differing by a
+reciprocal lattice vector produce the same phases, crystal momentum naturally lives in the
+dual of the translation lattice: the Brillouin zone.


Would it be more physical to call TranslationDual, BrilloinZone

I wasnt sure at what abstraction layer it should be called BrilloinZone but am now convinced its correct.

jstoobysmith · 2026-10-29T14:04:39Z

+/-! ## C. Action modulo translations -/
+
+/-- The symmetry action as a homomorphism to automorphisms of the character group. -/
+noncomputable def symmetryAction (C : Crystal G) :


Namespace or name could be more descriptive

…zone Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

TomOleDiem · 2026-10-30T14:17:04Z

I made a couple changes and added a new PR #1994 towards the concept of an irreducible Zone.
Naming should now be better, I didnt quite get what you meant by namespace.

TomOleDiem · 2026-10-30T14:17:12Z

-awaiting-author

jstoobysmith · 2026-10-30T17:28:11Z

+       map_mul' := fun _ _ => rfl } : Symmetry C →* Multiplicative (AddAut G))
+
+/-- Transforming momentum and lattice vector together keeps the value. -/
+lemma smul_lattice_apply {C : Crystal G} (s : Symmetry C) (k : BrillouinZone G) (a : G) :


Would these be better in the BrillouinZone namespace?

jstoobysmith · 2026-10-30T17:28:30Z

awaiting-author

…rillouinZone namespace Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

TomOleDiem · 2026-10-30T18:59:53Z

-awaiting-author

github-actions Bot added the medium label Oct 27, 2026

TomOleDiem changed the title ~~feat(CondensedMatter): action of crystal symmetries on translation characters~~ feat(CondensedMatter): action of crystal symmetries on dual group Oct 27, 2026

github-actions Bot added the t-condensed-matter Condensed matter label Oct 27, 2026

TomOleDiem force-pushed the feat/crystal-translation-dual branch 4 times, most recently from c6593e7 to dfde0eb Compare October 27, 2026 20:51

TomOleDiem marked this pull request as ready for review October 27, 2026 20:52

jstoobysmith reviewed Oct 29, 2026

View reviewed changes

jstoobysmith added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 29, 2026

TomOleDiem force-pushed the feat/crystal-translation-dual branch from dfde0eb to 27a732a Compare October 30, 2026 11:49

feat(CondensedMatter): action of crystal symmetries on the Brillouin …

832bd22

…zone Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

TomOleDiem force-pushed the feat/crystal-translation-dual branch from 0b82cf7 to 832bd22 Compare October 30, 2026 13:41

TomOleDiem changed the title ~~feat(CondensedMatter): action of crystal symmetries on dual group~~ feat(CondensedMatter): action of crystal symmetries on the Brillouin zone Oct 30, 2026

TomOleDiem mentioned this pull request Oct 30, 2026

feat(CondensedMatter): reduced zone and irreducible zones of a crystal #1994

Open

docs(CondensedMatter): cite an open-access source for the Brillouin zone

0555aab

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2026

jstoobysmith reviewed Oct 30, 2026

View reviewed changes

github-actions Bot added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2026

TomOleDiem and others added 2 commits October 30, 2026 19:54

refactor(CondensedMatter): move the symmetry action lemmas into the B…

2060855

…rillouinZone namespace Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

refactor(CondensedMatter): open Symmetry in the Brillouin zone file

6bdd292

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017zDwytmcJrWwVUR8jUpBSn

github-actions Bot removed the awaiting-author A reviewer has asked the author a question or requested changes label Oct 30, 2026

Navigation Menu

Repository navigation

feat(CondensedMatter): action of crystal symmetries on the Brillouin zone - #1975

feat(CondensedMatter): action of crystal symmetries on the Brillouin zone#1975
TomOleDiem wants to merge 4 commits into
leanprover-community:masterfrom
TomOleDiem:feat/crystal-translation-dual

TomOleDiem commented Oct 27, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Oct 27, 2026 •

edited

Loading

For the author: Please read

For reviewers: Summary of your PR

Uh oh!

jstoobysmith Oct 29, 2026

Uh oh!

jstoobysmith Oct 29, 2026

Uh oh!

TomOleDiem Oct 30, 2026

Uh oh!

jstoobysmith Oct 29, 2026

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

jstoobysmith Oct 30, 2026

Uh oh!

TomOleDiem Oct 30, 2026

Uh oh!

jstoobysmith commented Oct 30, 2026

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

TomOleDiem commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Uh oh!

github-actions Bot commented Oct 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

For the author: Please read

For reviewers: Summary of your PR

Uh oh!

jstoobysmith Oct 29, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Oct 29, 2026

Choose a reason for hiding this comment

Uh oh!

TomOleDiem Oct 30, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith Oct 29, 2026

Choose a reason for hiding this comment

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

jstoobysmith Oct 30, 2026

Choose a reason for hiding this comment

Uh oh!

TomOleDiem Oct 30, 2026

Choose a reason for hiding this comment

Uh oh!

jstoobysmith commented Oct 30, 2026

Uh oh!

TomOleDiem commented Oct 30, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

TomOleDiem commented Oct 27, 2026 •

edited

Loading

github-actions Bot commented Oct 27, 2026 •

edited

Loading